package systemf;


/*
 * Usage: substituteterm(value).as(name).into(body)
 *
 */
trait SubstitutionProvider {
  type VarID
  type VarRef
  type Term = LTerm
  type Type = LType
  type partial <: examplepartial
  //type full <: examplefull
  
  type topsubst <: exampletopsubst
  def removingBinder(ty:Type):Type
  
  def substituteterm(v:Term):partial
  def substitutetype(v:Type):partial
  abstract class examplepartial(v:Term){self : partial =>
    //def as(id: VarID): full
    def asTop: topsubst
    override def toString="[? := "+v+"]"
    
  }
  
  abstract class exampletopsubst(v:Term){self:topsubst =>
    def intoterm(term:Term):Term
    def intotype(ty:Type):Type
    override def toString="[top := "+v+"]"
  }
  
}
